{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators, GADTs,
  FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances,
  TypeSynonymInstances, EmptyDataDecls #-}

{-# OPTIONS_GHC -fcontext-stack=250 #-}

{- |

Module      :  Examples.InnerGeneric
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

The declaration that hook 'Examples.InnerBase.Inner' into @yoko@. This will
eventually be generated via Template Haskell.

-}
module Examples.InnerGeneric where

import qualified Examples.TermBase as B
import Examples.InnerBase (Inner)
import qualified Examples.InnerBase as I

import Examples.ReflectAux

data Lam; data Var; data App

concat `fmap` mapM derive [''Inner, ''Lam, ''Var, ''App]

type instance Tag Lam = $(return $ encode "Lam")
type instance Range Lam = Inner
instance DC Lam where
  occName _ = "Lam"
  fr ~(Lam ty tm) = I.Lam ty tm
data instance RM m (N Lam) = Lam B.Type (Med m Inner)
type instance Tag Var = $(return $ encode "Var")
type instance Range Var = Inner
instance DC Var where
  occName _ = "Var"
  fr ~(Var i) = I.Var i
data instance RM m (N Var) = Var Int
type instance Tag App = $(return $ encode "App")
type instance Range App = Inner
instance DC App where
  occName _ = "App"
  fr ~(App tm0 tm1) = I.App tm0 tm1
data instance RM m (N App) = App (Med m Inner) (Med m Inner)
data instance DCs Inner dc where
  Lam_ :: DCs Inner Lam; Var_ :: DCs Inner Var
  App_ :: DCs Inner App
type instance DTs Inner = InnerDTs
instance DT Inner where
  packageName _ = "datatype-reflect"
  moduleName _ = "InnerBase"
  disband (I.Lam ty tm)   = disbanded $ Lam ty tm
  disband (I.Var i)       = disbanded $ Var i
  disband (I.App tm0 tm1) = disbanded $ App tm0 tm1
type instance Fin (DCs Inner) = ((:=:) Lam :|| (:=:) Var) :|| (:=:) App
instance Finite (DCs Inner) where
  toFin Lam_ = membership; toFin Var_ = membership; toFin App_ = membership
  predFin _ _ x = x
instance Etinif (DCs Inner) where
  frFin x = case x of
    LeftU (LeftU  Refl) -> Lam_
    LeftU (RightU Refl) -> Var_
    RightU Refl -> App_

data InnerDTs t where Inner__ :: InnerDTs Inner
type instance Fin InnerDTs = (:=:) Inner
instance Finite InnerDTs where toFin Inner__ = Refl; predFin _ _ x = x
instance Etinif InnerDTs where frFin Refl = Inner__

finite_set [t|InnerDTs|]



type instance Rep Var = D Int :* U
instance Generic Var where
  rep ~(Var i) = D i :* U
  obj ~(D i :* U) = Var i
type instance Rep Lam = D B.Type :* R Inner :* U
instance Generic Lam where
  rep ~(Lam ty tm) = D ty :* R tm :* U
  obj ~(D ty :* R tm :* U) = Lam ty tm
type instance Rep App = R Inner :* R Inner :* U
instance Generic App where
  rep ~(App tm0 tm1) = R tm0 :* R tm1 :* U
  obj ~(R tm0 :* R tm1 :* U) = App tm0 tm1
